$\forall$$x$:Id, $k$:Knd, $A$, $T$:Type, $f$:($A$$\rightarrow$$T$$\rightarrow$$A$).
\\[0ex]$A$ $\Rightarrow$ $T$ $\Rightarrow$ AtomFree(Type;$A$) $\Rightarrow$ AtomFree(Type;$T$) $\Rightarrow$ Feasible(ma{-}single{-}effect0($x$;$A$;$k$;$T$;$f$))